Nuprl Lemma : Rlist-has-loc
0,22
postcript
pdf
L
:Top List,
i
:Top. R-has-loc(
(
L
);
i
) ~ reduce(
A
,
b
. R-has-loc(
A
;
i
)
b
;false
;
L
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Top
,
x
:
A
B
(
x
)
,
s
~
t
,
es
realizer
ind
Rplus
compseq
tag
def
,
R-has-loc(
R
;
i
)
,
(
L
)
,
es
realizer
ind
Rnone
compseq
tag
def
,
type
List
Lemmas
top
wf
origin
L:Top List, i:Top. R-has-loc(
(L);i) ~ reduce(
A,b. R-has-loc(A;i) 
b;false;L) L:Top List, i:Top. R-has-loc((L);i) ~ reduce(A,b. R-has-loc(A;i) b;false;L) 
Tx:A. B(x)
B(x)(L)